ecl-es-act(es;m;x)
== ecl_ind(x;k,test.e1,e2. False;a,b,aa,ab.e1,e2. aa(e1,e2)
==  e(e1,e2].ecl-es-halt(es;a)(0,e1,pred(e)) & ab(e,e2);a,b,aa,ab.e1,e2. aa(e1,e2)
== & necl-ex(b).e[e1,e2).ecl-es-halt(es;b)(n,e1,e)
==  ab(e1,e2) & necl-ex(a).e[e1,e2).ecl-es-halt(es;a)(n,e1,e);a,b,aa,ab.e1,e2. aa(e1,e2)
== & n0.ecl-ex(b).e[e1,e2).ecl-es-halt(es;b)(n,e1,e)
==  ab(e1,e2) & n0.ecl-ex(a).e[e1,e2).ecl-es-halt(es;a)(n,e1,e);a,aa.e1,e2.
== [e1;e2]~([x,y].ecl-es-halt(es;a)(0,x,y))*[x,y].aa
== [e1;e2]~([x,y].ecl-es-halt(es;a)(0,x,y))*[x,y].(x
== [e1;e2]~([x,y].ecl-es-halt(es;a)(0,x,y))*[x,y].,y);a,n,aa.if m=n ecl-es-halt(es;a)(0)
== [e1;e2]~([x,y].ecl-es-halt(es;a)(0,x,y))*[x,y].,y);a,n,aa.else aa fi;a,n,aa.aa;a,l,aa.aa) 

latex

---

clarification:

ecl-es-act(es;m;x)
== ecl_ind(x;k,test.e1,e2. False;a,b,aa,ab.e1,e2. aa(e1,e2)
==  existse-between3(es;e1;e2;e.ecl-es-halt(es;a)(0,e1,es-pred(es; e))
==  & ab(e,e2));a,b,aa,ab.e1,e2. aa(e1,e2)
== & necl-ex(b).alle-between1(es;e1;e2;e.ecl-es-halt(es;b)(n,e1,e))
==  ab(e1,e2) & necl-ex(a).alle-between1(es;e1;e2;e.ecl-es-halt(es;a)(n,e1,e));a,b,aa,ab.e1,e2.
== aa(e1,e2) & n0.ecl-ex(b).alle-between1(es;e1;e2;e.ecl-es-halt(es;b)(n,e1,e))
==  ab(e1,e2) & n0.ecl-ex(a).alle-between1(es;e1;e2;e.ecl-es-halt(es;a)(n,e1,e));a,aa.e1,e2.
== es-pstar-q(es;x,y.ecl-es-halt(es;a)
== es-pstar-q(es;x,y.(0
== es-pstar-q(es;x,y.,x
== es-pstar-q(es;x,y.,y);x,y.aa
== es-pstar-q(es;x,y.,y);x,y.(x
== es-pstar-q(es;x,y.,y);x,y.,y);e1;e2);a,n,aa.if m=n ecl-es-halt(es;a)(0)
== es-pstar-q(es;x,y.,y);x,y.,y);e1;e2);a,n,aa.else aa fi;a,n,aa.aa;a,l,aa.aa) 

latex

Definitions	ecl ind, False, e(e1,e2].P(e), pred(e), P  Q, P & Q, xL.P(x), car.cdr, ecl-ex(x), e[e1,e2).P(e), A, x.A(x), [e1;e2]~([a,b].p(a;b))*[a,b].q(a;b), if b t else f fi, i=j, f(a), ecl-es-halt(es;x), #$n
FDL editor aliases	ecl-es-act